• Keyword highlighting
• IntelliSense
• Model Explorer (F4)
• Go to Declaration Function (F12)  
• Find Usage
• Rename (F2)

A. The Keyword highlighting, as shown in the above figure, the keyword highlighting are explained as follows:

• the reserved keywords will be highlighted in blue.
• the processes names will be bold and highlighted in dark blue automatically.
• Symbols reserved for processes definition are shown in red.
• LTL formulars in assertions will be bold and shown in red.
• Comments are in green etc.

B. For the newly supported intelliSense, it can serve as an intelligent reminder for keywords when you are inputting your model:

• After you input an English letter for example 'a', it will automatically give out a list containing all keywords starting with 'a' and the explanation of the corresponding keyword. This is to better assist you in programming the model, and remind you the useful hints.
• After parsing the model, you will see the processes are also included in the list! See the figure above the process Specification() is in the list after checking grammar.

C. The Go to Declaration (F12) function is implemented for all variables, processes, constants, declarations and channels in all modules.

To use this function, follow the steps:
      Select a word in the editor and press F12, editor will bring you to the definition of the word if there is one.

D. The Model Explorer (F4) function is recently supported for all modules. Press F4 to open the explorer window and click refresh button, all the constants, variables, processes etc. will be shown in the list.  Parsing the model (by pressing F5) will also refresh the model explorer. To access a particular item, you only have to double click it. This function is extremely useful when the mode becomes quite big! 

E. Find Usage: This function is to help user to quickly locate all the usage of the selected text. It is useful especially in the large models with lots of variables, processes etc. To use this function, right click the selected text and choose the Find Usage label in the menu. For now, PAT is able to find usage for declarations, processes, variables, channels and constants in a model.

F. Rename (F2): Using renaming function when you want to sysmetically and safely change the name of a variable, it will automatically replace all the corresponding usage of the variable with the new name. To use this function, select a word (process name, variable, channel, constants and declaration) and press F2 (or right mouse click on the selected word and choose rename label in the menu). A popup window will show to ask for the new name. After you confirm, the changes will automatically apply to the whole model.

After input the model, the four key actions you can perform by click the corresponding buttons in the specification toolbar:

• Check Grammar : check whether the model has correct grammar. If the grammar is not accepted, there will be a pop-up of certain error message.
• Simulation : simulate the model using simulator. The grammar needs to be parsed first before the simulator to be shown.
• Verification : verify the assertions using verifier. The grammar needs to be parsed first before the verifier to be shown.
• Graph Difference: generate the graph grouping the similar states and transitions between two graphs. The grammar needs to be parsed first before the graph difference analysis to be shown.

PAT provides different user interface languages: Chinese (Simplified), Chinese (Traditional), English, Japanese, German and Vietnamese. You can switch between the languages under toolbar View->Languages. System will remember your choice next time it starts. Other languages will be added if there is a request.

The set of document editing functions are listed as follows:

• New: create a new model and open it in the Editor. New model wizard is also available now!
• Open: open an existing model.
• Save: save the model.
• Save As : save the model as another file.
• Email Model: email the current model to PAT team or friends.
• Print: print the model.
• LaTex Print: generate the LaTex text for the input model.
• Recent files: view your records of edited files recently.
• Exit: exit PAT by clicking it.

The set of text editing functions is listed as follows:

• Cut, Copy, Paste, Select All
• Find, Find Next, Replace
• Zoom in and Zoom out or 100% Text size 
• Redo, Undo
• Goto Line
• Comment Selected Code: Make a block of codes as a comment for reference.
• Uncomment Selected Code : Uncomment block of codes.
• Outlining: Toggle the selected codes or toggle all the outlining for a clear view of your model. You can expand them by click the '+' symbol by the side of line number.
• Bookmark: Add bookmarks to your code to memorise your ideas. You can view the previous or next bookmark as well as deleting all the bookmarks through the editing functions.

The set of featured editing functions is listed as follows:

• Line Number Display
• Highlight Current Line
• Go to Previous Tab
• Go to Next Tab
• Close Current Tab
• Drag and Drop a model into PAT to open it quickly